Left Termination of the query pattern
rotate(g,a)
w.r.t. the given Prolog program could successfully be proven:

0 Prolog
↳1 PrologToDTProblemTransformerProof (⇒, 86 ms)
↳2 TRIPLES
↳3 TriplesToPiDPProof (⇒, 35 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
    ↳7 PiDP
        ↳8 UsableRulesProof (⇔, 0 ms)
        ↳9 PiDP
        ↳10 PiDPToQDPProof (⇒, 33 ms)
        ↳11 QDP
        ↳12 QDPSizeChangeProof (⇔, 0 ms)
        ↳13 YES
    ↳14 PiDP
        ↳15 UsableRulesProof (⇔, 0 ms)
        ↳16 PiDP
        ↳17 PiDPToQDPProof (⇒, 0 ms)
        ↳18 QDP
        ↳19 QDPSizeChangeProof (⇔, 0 ms)
        ↳20 YES
    ↳21 PiDP
        ↳22 UsableRulesProof (⇔, 0 ms)
        ↳23 PiDP
        ↳24 PiDPToQDPProof (⇒, 0 ms)
        ↳25 QDP
        ↳26 QDPSizeChangeProof (⇔, 0 ms)
        ↳27 YES

(0) Obligation:

Clauses:

rotate(X, Y) :- ','(append2(A, B, X), append1(B, A, Y)).
append1(.(X, Xs), Ys, .(X, Zs)) :- append1(Xs, Ys, Zs).
append1([], Ys, Ys).
append2(.(X, Xs), Ys, .(X, Zs)) :- append2(Xs, Ys, Zs).
append2([], Ys, Ys).

Query: rotate(g,a)

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph DT10.

(2) Obligation:

Triples:

append2A(.(X1, X2), X3, .(X1, X4)) :- append2A(X2, X3, X4).
append1B(.(X1, X2), X3, X4, .(X1, X5)) :- append1B(X2, X3, X4, X5).
append1C(.(X1, X2), .(X1, X3)) :- append1C(X2, X3).
rotateD(.(X1, X2), X3) :- append2A(X4, X5, X2).
rotateD(.(X1, X2), X3) :- ','(append2cA(X4, X5, X2), append1B(X5, X1, X4, X3)).
rotateD(X1, X2) :- append1C(X1, X2).

Clauses:

append2cA(.(X1, X2), X3, .(X1, X4)) :- append2cA(X2, X3, X4).
append2cA([], X1, X1).
append1cB(.(X1, X2), X3, X4, .(X1, X5)) :- append1cB(X2, X3, X4, X5).
append1cB([], X1, X2, .(X1, X2)).
append1cC(.(X1, X2), .(X1, X3)) :- append1cC(X2, X3).
append1cC([], []).

Afs:

rotateD(x1, x2)  =  rotateD(x1)

(3) TriplesToPiDPProof (SOUND transformation)

We use the technique of [DT09]. With regard to the inferred argument filtering the predicates were used in the following modes:
rotateD_in: (b,f)
append2A_in: (f,f,b)
append2cA_in: (f,f,b)
append1B_in: (b,b,b,f)
append1C_in: (b,f)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

ROTATED_IN_GA(.(X1, X2), X3) → U4_GA(X1, X2, X3, append2A_in_aag(X4, X5, X2))
ROTATED_IN_GA(.(X1, X2), X3) → APPEND2A_IN_AAG(X4, X5, X2)
APPEND2A_IN_AAG(.(X1, X2), X3, .(X1, X4)) → U1_AAG(X1, X2, X3, X4, append2A_in_aag(X2, X3, X4))
APPEND2A_IN_AAG(.(X1, X2), X3, .(X1, X4)) → APPEND2A_IN_AAG(X2, X3, X4)
ROTATED_IN_GA(.(X1, X2), X3) → U5_GA(X1, X2, X3, append2cA_in_aag(X4, X5, X2))
U5_GA(X1, X2, X3, append2cA_out_aag(X4, X5, X2)) → U6_GA(X1, X2, X3, append1B_in_ggga(X5, X1, X4, X3))
U5_GA(X1, X2, X3, append2cA_out_aag(X4, X5, X2)) → APPEND1B_IN_GGGA(X5, X1, X4, X3)
APPEND1B_IN_GGGA(.(X1, X2), X3, X4, .(X1, X5)) → U2_GGGA(X1, X2, X3, X4, X5, append1B_in_ggga(X2, X3, X4, X5))
APPEND1B_IN_GGGA(.(X1, X2), X3, X4, .(X1, X5)) → APPEND1B_IN_GGGA(X2, X3, X4, X5)
ROTATED_IN_GA(X1, X2) → U7_GA(X1, X2, append1C_in_ga(X1, X2))
ROTATED_IN_GA(X1, X2) → APPEND1C_IN_GA(X1, X2)
APPEND1C_IN_GA(.(X1, X2), .(X1, X3)) → U3_GA(X1, X2, X3, append1C_in_ga(X2, X3))
APPEND1C_IN_GA(.(X1, X2), .(X1, X3)) → APPEND1C_IN_GA(X2, X3)

The TRS R consists of the following rules:

append2cA_in_aag(.(X1, X2), X3, .(X1, X4)) → U9_aag(X1, X2, X3, X4, append2cA_in_aag(X2, X3, X4))
append2cA_in_aag([], X1, X1) → append2cA_out_aag([], X1, X1)
U9_aag(X1, X2, X3, X4, append2cA_out_aag(X2, X3, X4)) → append2cA_out_aag(.(X1, X2), X3, .(X1, X4))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
append2A_in_aag(x1, x2, x3)  =  append2A_in_aag(x3)
append2cA_in_aag(x1, x2, x3)  =  append2cA_in_aag(x3)
U9_aag(x1, x2, x3, x4, x5)  =  U9_aag(x1, x4, x5)
append2cA_out_aag(x1, x2, x3)  =  append2cA_out_aag(x1, x2, x3)
append1B_in_ggga(x1, x2, x3, x4)  =  append1B_in_ggga(x1, x2, x3)
append1C_in_ga(x1, x2)  =  append1C_in_ga(x1)
ROTATED_IN_GA(x1, x2)  =  ROTATED_IN_GA(x1)
U4_GA(x1, x2, x3, x4)  =  U4_GA(x1, x2, x4)
APPEND2A_IN_AAG(x1, x2, x3)  =  APPEND2A_IN_AAG(x3)
U1_AAG(x1, x2, x3, x4, x5)  =  U1_AAG(x1, x4, x5)
U5_GA(x1, x2, x3, x4)  =  U5_GA(x1, x2, x4)
U6_GA(x1, x2, x3, x4)  =  U6_GA(x1, x2, x4)
APPEND1B_IN_GGGA(x1, x2, x3, x4)  =  APPEND1B_IN_GGGA(x1, x2, x3)
U2_GGGA(x1, x2, x3, x4, x5, x6)  =  U2_GGGA(x1, x2, x3, x4, x6)
U7_GA(x1, x2, x3)  =  U7_GA(x1, x3)
APPEND1C_IN_GA(x1, x2)  =  APPEND1C_IN_GA(x1)
U3_GA(x1, x2, x3, x4)  =  U3_GA(x1, x2, x4)

We have to consider all (P,R,Pi)-chains

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(4) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

ROTATED_IN_GA(.(X1, X2), X3) → U4_GA(X1, X2, X3, append2A_in_aag(X4, X5, X2))
ROTATED_IN_GA(.(X1, X2), X3) → APPEND2A_IN_AAG(X4, X5, X2)
APPEND2A_IN_AAG(.(X1, X2), X3, .(X1, X4)) → U1_AAG(X1, X2, X3, X4, append2A_in_aag(X2, X3, X4))
APPEND2A_IN_AAG(.(X1, X2), X3, .(X1, X4)) → APPEND2A_IN_AAG(X2, X3, X4)
ROTATED_IN_GA(.(X1, X2), X3) → U5_GA(X1, X2, X3, append2cA_in_aag(X4, X5, X2))
U5_GA(X1, X2, X3, append2cA_out_aag(X4, X5, X2)) → U6_GA(X1, X2, X3, append1B_in_ggga(X5, X1, X4, X3))
U5_GA(X1, X2, X3, append2cA_out_aag(X4, X5, X2)) → APPEND1B_IN_GGGA(X5, X1, X4, X3)
APPEND1B_IN_GGGA(.(X1, X2), X3, X4, .(X1, X5)) → U2_GGGA(X1, X2, X3, X4, X5, append1B_in_ggga(X2, X3, X4, X5))
APPEND1B_IN_GGGA(.(X1, X2), X3, X4, .(X1, X5)) → APPEND1B_IN_GGGA(X2, X3, X4, X5)
ROTATED_IN_GA(X1, X2) → U7_GA(X1, X2, append1C_in_ga(X1, X2))
ROTATED_IN_GA(X1, X2) → APPEND1C_IN_GA(X1, X2)
APPEND1C_IN_GA(.(X1, X2), .(X1, X3)) → U3_GA(X1, X2, X3, append1C_in_ga(X2, X3))
APPEND1C_IN_GA(.(X1, X2), .(X1, X3)) → APPEND1C_IN_GA(X2, X3)

The TRS R consists of the following rules:

append2cA_in_aag(.(X1, X2), X3, .(X1, X4)) → U9_aag(X1, X2, X3, X4, append2cA_in_aag(X2, X3, X4))
append2cA_in_aag([], X1, X1) → append2cA_out_aag([], X1, X1)
U9_aag(X1, X2, X3, X4, append2cA_out_aag(X2, X3, X4)) → append2cA_out_aag(.(X1, X2), X3, .(X1, X4))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
append2A_in_aag(x1, x2, x3)  =  append2A_in_aag(x3)
append2cA_in_aag(x1, x2, x3)  =  append2cA_in_aag(x3)
U9_aag(x1, x2, x3, x4, x5)  =  U9_aag(x1, x4, x5)
append2cA_out_aag(x1, x2, x3)  =  append2cA_out_aag(x1, x2, x3)
append1B_in_ggga(x1, x2, x3, x4)  =  append1B_in_ggga(x1, x2, x3)
append1C_in_ga(x1, x2)  =  append1C_in_ga(x1)
ROTATED_IN_GA(x1, x2)  =  ROTATED_IN_GA(x1)
U4_GA(x1, x2, x3, x4)  =  U4_GA(x1, x2, x4)
APPEND2A_IN_AAG(x1, x2, x3)  =  APPEND2A_IN_AAG(x3)
U1_AAG(x1, x2, x3, x4, x5)  =  U1_AAG(x1, x4, x5)
U5_GA(x1, x2, x3, x4)  =  U5_GA(x1, x2, x4)
U6_GA(x1, x2, x3, x4)  =  U6_GA(x1, x2, x4)
APPEND1B_IN_GGGA(x1, x2, x3, x4)  =  APPEND1B_IN_GGGA(x1, x2, x3)
U2_GGGA(x1, x2, x3, x4, x5, x6)  =  U2_GGGA(x1, x2, x3, x4, x6)
U7_GA(x1, x2, x3)  =  U7_GA(x1, x3)
APPEND1C_IN_GA(x1, x2)  =  APPEND1C_IN_GA(x1)
U3_GA(x1, x2, x3, x4)  =  U3_GA(x1, x2, x4)

We have to consider all (P,R,Pi)-chains

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 3 SCCs with 10 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

APPEND1C_IN_GA(.(X1, X2), .(X1, X3)) → APPEND1C_IN_GA(X2, X3)

The TRS R consists of the following rules:

append2cA_in_aag(.(X1, X2), X3, .(X1, X4)) → U9_aag(X1, X2, X3, X4, append2cA_in_aag(X2, X3, X4))
append2cA_in_aag([], X1, X1) → append2cA_out_aag([], X1, X1)
U9_aag(X1, X2, X3, X4, append2cA_out_aag(X2, X3, X4)) → append2cA_out_aag(.(X1, X2), X3, .(X1, X4))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
append2cA_in_aag(x1, x2, x3)  =  append2cA_in_aag(x3)
U9_aag(x1, x2, x3, x4, x5)  =  U9_aag(x1, x4, x5)
append2cA_out_aag(x1, x2, x3)  =  append2cA_out_aag(x1, x2, x3)
APPEND1C_IN_GA(x1, x2)  =  APPEND1C_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(8) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(9) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

APPEND1C_IN_GA(.(X1, X2), .(X1, X3)) → APPEND1C_IN_GA(X2, X3)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
APPEND1C_IN_GA(x1, x2)  =  APPEND1C_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(10) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(11) Obligation:

Q DP problem:
The TRS P consists of the following rules:

APPEND1C_IN_GA(.(X1, X2)) → APPEND1C_IN_GA(X2)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(12) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • APPEND1C_IN_GA(.(X1, X2)) → APPEND1C_IN_GA(X2)
    The graph contains the following edges 1 > 1

(13) YES

(14) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

APPEND1B_IN_GGGA(.(X1, X2), X3, X4, .(X1, X5)) → APPEND1B_IN_GGGA(X2, X3, X4, X5)

The TRS R consists of the following rules:

append2cA_in_aag(.(X1, X2), X3, .(X1, X4)) → U9_aag(X1, X2, X3, X4, append2cA_in_aag(X2, X3, X4))
append2cA_in_aag([], X1, X1) → append2cA_out_aag([], X1, X1)
U9_aag(X1, X2, X3, X4, append2cA_out_aag(X2, X3, X4)) → append2cA_out_aag(.(X1, X2), X3, .(X1, X4))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
append2cA_in_aag(x1, x2, x3)  =  append2cA_in_aag(x3)
U9_aag(x1, x2, x3, x4, x5)  =  U9_aag(x1, x4, x5)
append2cA_out_aag(x1, x2, x3)  =  append2cA_out_aag(x1, x2, x3)
APPEND1B_IN_GGGA(x1, x2, x3, x4)  =  APPEND1B_IN_GGGA(x1, x2, x3)

We have to consider all (P,R,Pi)-chains

(15) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(16) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

APPEND1B_IN_GGGA(.(X1, X2), X3, X4, .(X1, X5)) → APPEND1B_IN_GGGA(X2, X3, X4, X5)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
APPEND1B_IN_GGGA(x1, x2, x3, x4)  =  APPEND1B_IN_GGGA(x1, x2, x3)

We have to consider all (P,R,Pi)-chains

(17) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(18) Obligation:

Q DP problem:
The TRS P consists of the following rules:

APPEND1B_IN_GGGA(.(X1, X2), X3, X4) → APPEND1B_IN_GGGA(X2, X3, X4)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(19) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • APPEND1B_IN_GGGA(.(X1, X2), X3, X4) → APPEND1B_IN_GGGA(X2, X3, X4)
    The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 3

(20) YES

(21) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

APPEND2A_IN_AAG(.(X1, X2), X3, .(X1, X4)) → APPEND2A_IN_AAG(X2, X3, X4)

The TRS R consists of the following rules:

append2cA_in_aag(.(X1, X2), X3, .(X1, X4)) → U9_aag(X1, X2, X3, X4, append2cA_in_aag(X2, X3, X4))
append2cA_in_aag([], X1, X1) → append2cA_out_aag([], X1, X1)
U9_aag(X1, X2, X3, X4, append2cA_out_aag(X2, X3, X4)) → append2cA_out_aag(.(X1, X2), X3, .(X1, X4))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
append2cA_in_aag(x1, x2, x3)  =  append2cA_in_aag(x3)
U9_aag(x1, x2, x3, x4, x5)  =  U9_aag(x1, x4, x5)
append2cA_out_aag(x1, x2, x3)  =  append2cA_out_aag(x1, x2, x3)
APPEND2A_IN_AAG(x1, x2, x3)  =  APPEND2A_IN_AAG(x3)

We have to consider all (P,R,Pi)-chains

(22) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(23) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

APPEND2A_IN_AAG(.(X1, X2), X3, .(X1, X4)) → APPEND2A_IN_AAG(X2, X3, X4)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
APPEND2A_IN_AAG(x1, x2, x3)  =  APPEND2A_IN_AAG(x3)

We have to consider all (P,R,Pi)-chains

(24) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(25) Obligation:

Q DP problem:
The TRS P consists of the following rules:

APPEND2A_IN_AAG(.(X1, X4)) → APPEND2A_IN_AAG(X4)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(26) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • APPEND2A_IN_AAG(.(X1, X4)) → APPEND2A_IN_AAG(X4)
    The graph contains the following edges 1 > 1

(27) YES